(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(assert v2)
(push)
(assert (=> (=> v2 v1) (=> v2 v1)))
(assert (not (xor (=> v2 v1) v1 v2 v2 v0 (=> v2 v1) v2 (=> v2 v1) (=> v2 v1) v2 (=> v2 v1))))
(push)
(assert (distinct v2 v0 v2))
(pop)
(pop)
(assert v1)
(declare-const v3 Bool)
(assert (=> v2 v1))
(push)
(assert v1)
(declare-const v4 Bool)
(declare-const v5 Bool)
(push)
(declare-const v6 Bool)
(declare-const v7 Bool)
(assert (=> v2 v1))
(assert v3)
(push)
(declare-const v8 Bool)
(pop)
(assert (and v3 v6 (=> (not (xor (=> v2 v1) v1 v2 v2 v0 (=> v2 v1) v2 (=> v2 v1) (=> v2 v1) v2 (=> v2 v1))) v3) v5 (= (_ bv466 9) (bvneg (_ bv466 9)) (_ bv466 9) (bvnand (bvneg (_ bv466 9)) (bvneg (_ bv466 9)))) (=> (not (xor (=> v2 v1) v1 v2 v2 v0 (=> v2 v1) v2 (=> v2 v1) (=> v2 v1) v2 (=> v2 v1))) v3) v3))
(declare-const v9 Bool)
(declare-const _11-0 (_ BitVec 11))
(assert (not v0))
(declare-const v10 Bool)
(pop)
(check-sat)
(pop)
(push)
(declare-const v11 Bool)
(assert (not v2))
(check-sat)
